#ifndef __SOLVER_KERNEL_H__
#define __SOLVER_KERNEL_H__

#include "solver_function.h"
#include "vec.h"

__global__ void
//__launch_bounds__ ( __threadsPerBlock, __minBlocksPerMultiprocessor )
kernel_dpll_sat( void )
{
	int tId = threadIdx.x;
	int bId = blockIdx.x;

	if ( get_satResult( bId ).convert_to_int() != __LBOOL_UNDEF_INT )
	{ return; }

	__shared__ Lbool*			tVarAssignment;
	__shared__ int*				tVarOrder;
	__shared__ Lit**			tWatchPointer;
	__shared__ Lit*				tTrail;
	__shared__ int*				tDecisionLevel;
	__shared__ bool*			tVarSeenMarker;
	__shared__ Clause**			tAntecedentPointer;

	__shared__ Vec <Clause*>*	tWatchList;

#ifdef RANDOM_POLARITY
	__shared__ curandState		localCurandState;
#endif
	__shared__ volatile int		unitClauseSize;
	__shared__ volatile int		unitAssumptionCount;
	__shared__ unsigned int		conflictCount;
	__shared__ unsigned int		conflictCountLimit;
	__shared__ unsigned int		decisionCount;
	__shared__ unsigned int		propagationCount;
	__shared__ unsigned int		conflictLitCount;

	__shared__ int				decisionLevel;
	__shared__ int				trailEndId;

	__shared__ Vec <Lit>* localUnitClausePtr;
	__shared__ Vec <int>* decisionLevelVarOrderPtr; // For back-tracking.
	__shared__ Vec <int>* decisionLevelTrailIdPtr; // For back-tracking.
	__shared__ Vec <Lit>* propagationQueuePtr;
	__shared__ Vec <Lit>* tempQueuePtr;
	__shared__ Vec <Clause*>* antecedentQueuePtr;
	__shared__ Vec <Clause*>* tempAntecedentPtr;
	__shared__ Vec <Clause*>* tempWatchListPtr;
	__shared__ Vec <Lit>* learntClauseLitPtr;

	__shared__ int						order;
	__shared__ volatile bool			doBCP;
	__shared__ volatile bool			doConflictAnalysis;
	__shared__ volatile unsigned int	counter;

	if ( tId == 0 )
	{
		tVarAssignment = (Lbool*)( (char*)__dev_varAssignment + bId * __dev_varAssignmentPitch );
		tVarOrder = (int*)( (char*)__dev_varOrder + bId * __dev_varOrderPitch );
		tWatchPointer =  (Lit**)( (char*)__dev_watchPointer + bId * __dev_watchPointerPitch );
		tTrail = (Lit*)( (char*)__dev_trail + bId * __dev_trailPitch );
		tDecisionLevel = (int*)( (char*)__dev_decisionLevel + bId * __dev_decisionLevelPitch );
		tVarSeenMarker = (bool*)( (char*)__dev_varSeenMarker + bId * __dev_varSeenMarkerPitch );
		tAntecedentPointer = (Clause**)( (char*)__dev_antecedentPointer + bId * __dev_antecedentPointerPitch );

		tWatchList = get_watchListPtr( bId );

#ifdef RANDOM_POLARITY
		localCurandState = __dev_randState[bId];
#endif
		unitClauseSize = atomicMax( &__dev_unitClauseLitSize, 0 );
		unitAssumptionCount = 0;
		conflictCount = get_conflictCount( bId );
		conflictCountLimit = __dev_conflictLimit;
		decisionCount = get_decisionCount( bId );
		propagationCount = get_propagationCount( bId );
		conflictLitCount = get_conflictLitCount( bId );
		decisionLevel = 0;
		trailEndId = 0;

#ifdef DEBUG_CUDASAT
		printf( "tId #%d bId #%d: conflictCount = %d, conflictCountLimit = %d\n", tId, bId, conflictCount, conflictCountLimit );
#endif
		localUnitClausePtr = __dev_localUnitClausePtr[bId];
		decisionLevelVarOrderPtr = __dev_decisionLevelVarOrderPtr[bId];
		decisionLevelTrailIdPtr = __dev_decisionLevelTrailIdPtr[bId];
		propagationQueuePtr = __dev_propagationQueuePtr[bId];
		tempQueuePtr = __dev_tempQueuePtr[bId];
		antecedentQueuePtr = __dev_antecedentQueuePtr[bId];
		tempAntecedentPtr = __dev_tempAntecedentPtr[bId];
		tempWatchListPtr = __dev_tempWatchListPtr[bId];
		learntClauseLitPtr = __dev_learntClauseLitPtr[bId];

		localUnitClausePtr->clear();
		decisionLevelVarOrderPtr->clear();
		decisionLevelTrailIdPtr->clear();
		propagationQueuePtr->clear();
		tempQueuePtr->clear();
		antecedentQueuePtr->clear();
		tempAntecedentPtr->clear();
		tempWatchListPtr->clear();
		learntClauseLitPtr->clear();

		for ( int i = 0; i < unitClauseSize; ++i )
		{ localUnitClausePtr->push_back( get_unitClauseLit(i) ); }
#ifdef DEBUG_CUDASAT
		printf( "tId #%d, bId #%d: unitClauseSize = %d, localUnitClausePtr->size() = %d\n", tId, bId, unitClauseSize, localUnitClausePtr->size() );
#endif

		decisionLevelVarOrderPtr->push_back(-1);
		decisionLevelTrailIdPtr->push_back(0);

		order = 0;
		doBCP = false;
		doConflictAnalysis = false;
		counter = 0;
	} // if ( tId == 0 )
	__threadfence_block();
	//__syncthreads();

	while ( order < __dev_varNumber )
	{
		__shared__ int hasResult;
#ifdef HALF_IDLE_BLOCK
		__shared__ int idleCount;
#endif
		if ( tId == 0 )
		{
			hasResult = atomicMax( &__dev_hasResult, 0 );
#ifdef HALF_IDLE_BLOCK
			idleCount = atomicMax( &__dev_idleBlockCount, 0 );
#endif
		} // if ( tId == 0 )
		__threadfence_block();

		if ( hasResult > 0 )
		{ break; }
#ifdef HALF_IDLE_BLOCK
		if ( idleCount > (__blocksPerGrid >> 1) )
		{ break; }
#endif
		if ( tId == 0 )
		{ ++counter; }
		__threadfence_block();
/*
		if ( counter > (__dev_varNumber << 10) )
		{
			printf( "tId #%d bId #%d: counter = %d. Too many iterations, stop.\n", tId, bId, counter );
			break;
		}
*/
		__shared__ volatile bool swapVarOrder;
		__shared__ volatile bool continueLoop;
		__shared__ volatile bool stopLoop;
		__shared__ int unitVar;
		__shared__ int varId;

		if ( tId == 0 )
		{
			unitClauseSize = localUnitClausePtr->size();
			swapVarOrder = false;
			continueLoop = false;
			stopLoop = false;
			varId = get_varOrder( tVarOrder, order );
			__threadfence_block();

			if ( order < unitClauseSize )
			{
				unitVar = localUnitClausePtr->at(order).var();
				__threadfence_block();
#ifdef ASSERT
				if ( unitVar < 0 )
				{
					printf( "tId #%d bId #%d: Assertion failed: unitVar = %d, order = %d, unitClauseSize = %d\n", tId, bId, unitVar, order, unitClauseSize );
					stopLoop = true;
					__threadfence_block();
				}
#endif
#ifdef DEBUG_CUDASAT
				printf( "tId #%d bId #%d: varId = %d, unitVar = %d\n", tId, bId, varId, unitVar );
#endif
				if ( varId != unitVar )
				{
					swapVarOrder = true;
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: swapVarOrder = true\n", tId, bId );
#endif
				}
			}
		} // if ( tId == 0 )
		__threadfence_block();
		//__syncthreads();

		if ( swapVarOrder == true )
		{
			__shared__ int position;
			
			if ( tId == 0 )
			{ position = order; }
			__threadfence_block();

			for ( int i = tId; i < __dev_varNumber; i += __threadsPerBlock )
			{
				if ( get_varOrder( tVarOrder, i ) == unitVar )
				{
					position = i;
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: found swap position = %d.\n", tId, bId, i );
#endif
					__threadfence_block();
					break;
				}

				if ( position != order )
				{ break; }
			}
			__threadfence_block();

			if ( tId == 0 )
			{
				if ( position == order )
				{
#ifdef ASSERT
					printf( "tId #%d bId #%d: Assertion fail: swapping varOrder position of unitVar #%d is not found.\n", tId, bId, unitVar );
#endif
				}
				else
				{
					set_varOrder( tVarOrder, order, unitVar );
					set_varOrder( tVarOrder, position, varId );
				}
#ifdef DEBUG_CUDASAT
				printf( "tId #%d bId #%d: Swapped. tVarOrder[%d] = %d, tVarOrder[%d] = %d\n", tId, bId, order, get_varOrder( tVarOrder, order ), position, get_varOrder( tVarOrder, position ) );
#endif
			} // if ( tId == 0 )
			__threadfence_block();
			//__syncthreads();
			if ( tId == 0 )
			{ varId = unitVar; }
			__threadfence_block();
		} // if ( swapVarOrder == true )
		__threadfence_block();

		if ( tId == 0 )
		{
			if ( (get_varAssignment( tVarAssignment, get_varOrder( tVarOrder, order ) )).convert_to_int() != __LBOOL_UNDEF_INT )
			{
				++order;
				continueLoop = true;
			}
		}
		__threadfence_block();

		if ( get_satResult( bId ).convert_to_int() == __LBOOL_FALSE_INT )
		{ break; }

		if ( continueLoop == true )
		{ continue; }

		// Propagate unit clauses from input.
		if ( tId == 0 )
		{
			// For some unknown reason, sometimes these Vec won't be clean after each decision loop completed.
			propagationQueuePtr->clear();
			antecedentQueuePtr->clear();
			__threadfence_block();
#ifdef DEBUG_CUDASAT
			printf( "tId #%d bId #%d: order = %d, varId = %d\n", tId, bId, order, varId );
#endif
			// Decision level = 0.
			if ( unitAssumptionCount < unitClauseSize )
			{
#ifdef ASSERT
				if ( decisionLevel != 0 )
				{ printf( "tId #%d bId #%d: Assertion failed: decisionLevel = %d != 0 in unit order. Set it to 0.\n", tId, bId, decisionLevel ); }
				decisionLevel = 0;
				__threadfence_block();
#endif
				// These literals must be true. But it will be assigned false later. Thus we use inverse here.
				propagationQueuePtr->push_back( ~(localUnitClausePtr->at(unitAssumptionCount)) );
				++unitAssumptionCount;
				__threadfence_block();
#ifdef ASSERT
				if ( propagationQueuePtr->back().index() < 0 )
				{
					printf( "tId #%d bId #%d: Assertion failed: propagationQueuePtr->back().index() = %d\n", tId, bId, propagationQueuePtr->back().index() );
					stopLoop = true;
					__threadfence_block();
				}
#endif
#ifdef DEBUG_CUDASAT
				printf( "tId #%d bId #%d: propagationQueuePtr->push_back(unit Lit #%d)\n", tId, bId, get_unitClauseLit(order).index() );
#endif
			}
			else // Make decision.
			{
				++decisionLevel;
				++decisionCount;
				__threadfence_block();
#ifdef RANDOM_POLARITY
				bool polarity = (bool)( curand( &localCurandState ) & 0x00000001 );
				if ( polarity == true )
				{ propagationQueuePtr->push_back( Lit(varId) ); }
				else
				{ propagationQueuePtr->push_back( Lit(varId, true) ); }
				__threadfence_block();
#else
				propagationQueuePtr->push_back( Lit(varId) );
				__threadfence_block();
#endif

#ifdef DEBUG_CUDASAT
				printf( "tId #%d bId #%d: propagationQueuePtr->push_back(Lit #%d)\n", tId, bId, (propagationQueuePtr->back()).index() );
#endif
			}

			antecedentQueuePtr->push_back(NULL); // A dummy for no antecedent clause.
			__threadfence_block();
#ifdef DEBUG_CUDASAT
			printf( "tId #%d bId #%d: decision level = %d, trailEndId = %d\n", tId, bId, decisionLevel, trailEndId );
#endif

#ifdef ASSERT
			if ( propagationQueuePtr->empty() == true )
			{ printf( "tId #%d bId #%d: Assertion failed: propagationQueuePtr->empty() == true at decisionLevel = %d after decision or unit constant\n", tId, bId, decisionLevel ); }
#endif
			doBCP = true;

			tempQueuePtr->clear();
			tempAntecedentPtr->clear();
			tempWatchListPtr->clear();
		} // if ( tId == 0 )
		__threadfence_block();
		//__syncthreads();
#ifdef ASSERT
		if ( stopLoop == true )
		{ break; }
#endif
		while ( doBCP == true )
		{
			__shared__ Lit lit;
			__shared__ Clause* antecedentPtr;
			__shared__ Vec <Clause*>* oldWatchListPtr;
			__shared__ volatile int threadCount;
			__shared__ Clause* conflictClausePtr;

			if ( tId == 0 )
			{
#ifdef DEBUG_CUDASAT
				printf( "tId #%d bId #%d: doBCP == true\n" );
#endif
				doBCP = false;
				doConflictAnalysis = false;
				__threadfence_block();

				while ( (propagationQueuePtr->empty() == false) && (doBCP == false) )
				{
#ifdef ASSERT
					if ( propagationQueuePtr->size() != antecedentQueuePtr->size() )
					{ printf( "tId #%d bId #%d: Assertion failed: propagationQueue and antecedentQueue size are not matched.\n", tId, bId ); }
#endif
					lit = propagationQueuePtr->front();
					antecedentPtr = antecedentQueuePtr->front();

					propagationQueuePtr->erase(0);
					antecedentQueuePtr->erase(0);

					__threadfence_block();

					if ( lit.value( get_varAssignment( tVarAssignment, lit.var() ) ).convert_to_int() == __LBOOL_UNDEF_INT )
					{ doBCP = true; }
					__threadfence_block();
				} // while ( (propagationQueuePtr->empty() == false) && (doBCP == false) )

				if ( doBCP == true )
				{
#ifdef ASSERT
					if ( (lit.index() < 0) || (lit.index() >= __dev_litNumber) )
					{
						stopLoop = true;
						__threadfence_block();
						printf( "tId #%d bId #%d: Assertion failed: lit.index() = %d\n", lit.index() );
						break;
					}
#endif
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: propagationQueue pop front. Lit #%d\n", tId, bId, lit.index() );
#endif
					// Make this literal to be false.
					set_varAssignment( tVarAssignment, lit.var(), lit.false_var_ass() );
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: tVarAssignment[%d] = %d\n", tId, bId, lit.var(), (get_varAssignment(tVarAssignment, lit.var() )).convert_to_int() );
#endif
					set_decisionLevel( tDecisionLevel, lit.var(), decisionLevel );
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: tDecisionLevel[%d] = %d\n", tId, bId, lit.var(), decisionLevel );
#endif
					set_antecedentPointer( tAntecedentPointer, lit.var(), antecedentPtr );
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: tAntecedentPointer[%d] = %x, clause index = %d\n", tId, bId, trailEndId, get_antecedentPointer( tAntecedentPointer, lit.var() ),
						((get_antecedentPointer( tAntecedentPointer, lit.var() ) == NULL) ? -1 : get_antecedentPointer( tAntecedentPointer, lit.var() )->index()) );
#endif
					set_trail( tTrail, trailEndId, lit );
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: tTrail[%d] = Lit #%d\n", tId, bId, trailEndId, lit.index() );
#endif
					// Attention! trailEndId can't be an index after this line.
					++trailEndId;
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: ++trailEndId. trailEndId = %d\n", tId, bId, trailEndId );
#endif
					++propagationCount;

					if ( decisionLevel >= decisionLevelVarOrderPtr->size() )
					{ decisionLevelVarOrderPtr->push_back( order ); }
					else
					{ decisionLevelVarOrderPtr->at(decisionLevel) = order; }

					if ( decisionLevel >= decisionLevelTrailIdPtr->size() )
					{ decisionLevelTrailIdPtr->push_back( trailEndId ); }
					else
					{ decisionLevelTrailIdPtr->at(decisionLevel) = trailEndId; }
					__threadfence_block();

					oldWatchListPtr = get_watchList( tWatchList, lit.index() );
					oldWatchListPtr->move_to( *tempWatchListPtr );

					threadCount = tempWatchListPtr->size();
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: threadCount = %d\n", tId, bId, threadCount );
#endif
				} // if ( doBCP == true )
			} // if ( tId == 0 )
			__threadfence_block();
			//__syncthreads();

			// For every thread. No valid literal in queue.
			if ( doBCP == false )
			{ break; } // BREAK: while ( doBCP == true )

			int size = tempWatchListPtr->size();

			for ( int i = tId; i < size; i += __threadsPerBlock )
			{
				// Result: 0 = do nothing, -1 = conflict, 1 = implication.
				__shared__ int		result		[__threadsPerBlock];
				__shared__ Lit		imply		[__threadsPerBlock];
				__shared__ Clause*	clausePtr	[__threadsPerBlock];
				__shared__ Lit*		newWatch	[__threadsPerBlock];
				__shared__ Lit*		watch2		[__threadsPerBlock];
				__shared__ bool		foundNew	[__threadsPerBlock];

				volatile bool swapWatch = false;

				result[tId] = 0;
				imply[tId] = Lit();
				clausePtr[tId] = tempWatchListPtr->at(i);
#ifdef ASSERT
				if ( tempWatchListPtr->at(i) == NULL )
				{ printf( "tId #%d bId #%d: Assertion failed: tempWatchListPtr->at(%d) == NULL, lit #%d\n", i, lit.index() ); }
#endif
				foundNew[tId] = false;
#ifdef DEBUG_CUDASAT
				printf( "tId #%d bId #%d: tempWatchListPtr->at(%d) = %x, clause index = %d\n", tId, bId, i, tempWatchListPtr->at(i), (tempWatchListPtr->at(i))->index() );
#endif
				newWatch[tId] = get_watchPointer( tWatchPointer, ((clausePtr[tId]->index()) << 1) );
				watch2[tId] = get_watchPointer( tWatchPointer, (((clausePtr[tId]->index()) << 1) + 1) );
				__threadfence_block();
#ifdef DEBUG_CUDASAT
				printf( "tId #%d bId #%d: newWatch[%d] = %x (Lit #%d), watch2[%d] = %x, (Lit #%d)\n", tId, bId, tId, newWatch[tId], (*newWatch[tId]).index(), tId, watch2[tId], (*watch2[tId]).index() );
#endif
				if ( (*newWatch[tId]) != lit )
				{
					watch2[tId] = (Lit*)atomicExch( (unsigned int*)&newWatch[tId], (unsigned int)watch2[tId] );
					swapWatch = true;
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: swapWatch = %d, swap newWatch[%d] and watchPtr2\n", tId, bId, swapWatch, tId );
#endif
				}
#ifdef ASSERT
				if ( (*newWatch[tId]) != lit )
				{
					printf( "tId #%d bId #%d: Assertion failed: (*newWatch[%d] = Lit #%d) != lit #%d\n", tId, bId, tId, (*newWatch[tId]).index(), lit.index() );
					stopLoop = true;
					__threadfence_block();
				}
#endif
#ifdef DEBUG_CUDASAT
				printf( "tId #%d bId #%d: newWatch[%d] = %x (Lit #%d), watch2[%d] = %x, (Lit #%d)\n", tId, bId, tId, newWatch[tId], (*newWatch[tId]).index(), tId, watch2[tId], (*watch2[tId]).index() );
#endif
				for ( int j = 0; j < clausePtr[tId]->size(); ++j )
				{
					Lit* claLitPtr = clausePtr[tId]->data_pointer(j);

					if ( (claLitPtr == newWatch[tId]) || (claLitPtr == watch2[tId]) )
					{ continue; }

					if ( claLitPtr->value( get_varAssignment( tVarAssignment, claLitPtr->var() ) ).convert_to_int()
						!= __LBOOL_FALSE_INT )
					{
						newWatch[tId] = claLitPtr;
						foundNew[tId] = true;
#ifdef DEBUG_CUDASAT
						printf( "tId #%d bId #%d: found == true, newWatch[%d] = %x (Lit #%d)\n", tId, bId, tId, claLitPtr, claLitPtr->index() );
#endif
						break;
					}
				}
				__threadfence_block();

				if ( foundNew[tId] == false )
				{
					if ( watch2[tId]->value( get_varAssignment( tVarAssignment, watch2[tId]->var() ) ).convert_to_int()
						== __LBOOL_FALSE_INT )
					{ result[tId] = -1; }
					else if ( watch2[tId]->value( get_varAssignment( tVarAssignment, watch2[tId]->var() ) ).convert_to_int()
						== __LBOOL_UNDEF_INT )
					{
						result[tId] = 1;
						// This will be assigned to be false during assignment.
						// Thus it needs to be inverse literal here.
						imply[tId] = ~(*watch2[tId]);
					}
				}
				else // ( foundNew[tId] == true )
				{
					if ( swapWatch == false )
					{ set_watchPointer( tWatchPointer, (clausePtr[tId]->index() << 1), newWatch[tId] ); }
					else
					{ set_watchPointer( tWatchPointer, ((clausePtr[tId]->index() << 1) + 1), newWatch[tId] ); }
#ifdef ASSERT
					if ( get_watchPointer( tWatchPointer, (clausePtr[tId]->index() << 1) )
						== get_watchPointer( tWatchPointer, ((clausePtr[tId]->index() << 1) + 1) ) )
					{ printf( "tId #%d bId #%d: Assertion failed: updated two watch pointers are identical.\n", tId, bId ); }
#endif
				}
				__syncthreads();

				// Check result for each thread. Can't parallel here for vectors' push back.
				if( tId == 0 )
				{
					int size = (threadCount > __threadsPerBlock) ? __threadsPerBlock : threadCount;
					threadCount -= __threadsPerBlock;
					__threadfence_block();
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: size = %d, threadCount = %d\n", tId, bId, size, threadCount );
#endif
					for ( int j = 0; j < size; ++j )
					{
						if ( (*newWatch[j]) == lit )
						{ oldWatchListPtr->push_back( clausePtr[j] ); }
						else
						{ (get_watchList( tWatchList, newWatch[j]->index() ))->push_back( clausePtr[j] ); }
						__threadfence_block();
#ifdef DEBUG_CUDASAT
						printf( "tId #%d bId #%d: tWatchList[%d] push_back(clause %x, clause index = %d)\n", tId, bId, newWatch[j]->index(), clausePtr[j], clausePtr[j]->index() );
						printf( "tId #%d bId #%d: result[%d] = %d\n", tId, bId, tId, result[j] );
#endif
						if ( doConflictAnalysis == false )
						{
							if ( result[j] == -1 )
							{
								doConflictAnalysis = true;
								conflictClausePtr = clausePtr[j];
								__threadfence_block();
#ifdef DEBUG_CUDASAT
								printf( "tId #%d bId #%d: doConflictAnalysis = true, clausePtr[%d] = %x, clause index = %d\n", tId, bId, j, (void*)clausePtr[j], clausePtr[j]->index() );
#endif
#ifdef ASSERT
								if ( conflictClausePtr == NULL )
								{ printf("tId #%d bId #%d: (1) conflictClausePtr == NULL\n", tId, bId ); }
#endif
							}
							else if ( result[j] == 1 )
							{
								tempQueuePtr->push_back( imply[j] );
								tempAntecedentPtr->push_back( clausePtr[j] );
								__threadfence_block();
#ifdef ASSERT
								if ( clausePtr[j] == NULL )
								{ printf("tId #%d bId #%d: tempAntecedentPtr->push_back( clausePtr[%d] == NULL )\n", tId, bId, j ); }
#endif
							}
						}
					}
					// Restore the clause pointers in watch list behind conflict clause.
					if ( (doConflictAnalysis == true) && (threadCount > 0) )
					{
						for ( int j = (tempWatchListPtr->size() - 1); j > (tempWatchListPtr->size() - 1 - threadCount); --j )
						{
							oldWatchListPtr->push_back( tempWatchListPtr->at(j) );
							__threadfence_block();
						}
					}
				} // if( tId == 0 )
				__threadfence_block();
				//__syncthreads();
#ifdef ASSERT
				if ( stopLoop == true )
				{ break; }
#endif
				if ( doConflictAnalysis == true )
				{ break; }
			} // for ( int i = tId; i < tempWatchListPtr->size(); i += __threadsPerBlock )
			__threadfence_block();
			//__syncthreads();
#ifdef ASSERT
			if ( stopLoop == true )
			{ break; }
#endif
			if ( tId == 0 )
			{
				if ( doConflictAnalysis == false )
				{
					if ( trailEndId == __dev_varNumber )
					{
						set_satResult( bId, Lbool(true) );
#ifdef DEBUG_CRITICAL
						printf( "tId #%d bId #%d: (1) checked SAT.\n", tId, bId );
#endif
						__threadfence_block();
						break;
					}

					for ( int i = 0; i < tempQueuePtr->size(); ++i )
					{
						propagationQueuePtr->push_back( tempQueuePtr->at(i) );
						antecedentQueuePtr->push_back( tempAntecedentPtr->at(i) );
						__threadfence_block();
#ifdef DEBUG_CUDASAT
						printf( "tId #%d bId #%d: propagationQueuePtr->push_back(Lit #%d)\n", tId, bId, (tempQueuePtr->at(i)).index() );
						printf( "tId #%d bId #%d: antecedentQueuePtr->push_back(Clause* %x, index = %d)\n", tId, bId, (void*)(tempAntecedentPtr->at(i)), (tempAntecedentPtr->at(i))->index() );
#endif
					}
					__threadfence_block();

					if ( propagationQueuePtr->empty() == false )
					{ doBCP = true; }
					else
					{
						doBCP = false;
#ifdef DEBUG_CUDASAT
						if ( propagationQueuePtr->empty() == true )
						{ printf( "tId #%d bId #%d: propagationQueue is empty at the end of BCP. do BCP = %d\n", tId, bId, doBCP ); }
#endif
					}
				}
				else
				{
					++conflictCount;
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: doConflictAnalysis = true. conflictCount = %d, doBCP = false.\n", tId, bId, conflictCount );
#endif
				}
				__threadfence_block();
			} // if ( tId == 0 )
			__threadfence_block();
			//__syncthreads();

			if ( get_satResult( bId ).convert_to_int() == __LBOOL_TRUE_INT )
			{ break; }

			// A little different from MiniSat 1.14 since our trail is somewaht different.
			if ( doConflictAnalysis == true )
			{
				if ( decisionLevel == 0 )
				{
					if ( tId == 0 )
					{
						set_satResult( bId, Lbool(false) );
#ifdef DEBUG_CRITICAL
						printf( "tId #%d bId #%d: (2) checked UNSAT.\n", tId, bId );
#endif
					}
					__threadfence_block();
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: conflict at level 0. UNSAT.\n", tId, bId );
#endif
					break;
				}
				// Attention! trailEndId is like iterator end, that is beyond the last element and can't be used as an index.
#ifdef DEBUG_CUDASAT
				if ( tId == 0 )
				{
					printf( "tId #%d bId #%d: doConflictAnalysis == true\n", tId, bId );
					//printf( "tId #%d bId #%d: order = %d, decisionLevel = %d, trailBeginId = %d, trailEndId = %d\n", tId, bId, order, decisionLevel, trailBeginId, trailEndId );
					printf( "tId #%d bId #%d: order = %d, decisionLevel = %d, trailEndId = %d\n", tId, bId, order, decisionLevel, trailEndId );
				}
#endif
				// Initialize __dev_varSeenMarker
				for ( int i = tId; i < __dev_varNumber; i += __threadsPerBlock )
				{ set_varSeenMarker( tVarSeenMarker, i, false ); }
				__threadfence_block();

				__shared__ volatile int maxLearntLitLevel;

				if ( tId == 0 )
				{
					maxLearntLitLevel = 0;

					volatile int index = trailEndId;
					Lit conflictLit = get_trail( tTrail, index - 1 );
					Lit currentTrailLit = ~(conflictLit);
					volatile int implicationPointCount = 1;
					Clause* clausePtr = conflictClausePtr;

					learntClauseLitPtr->clear();
					set_varSeenMarker( tVarSeenMarker, currentTrailLit.var(), true );
					__threadfence_block();
					learntClauseLitPtr->push_back( Lit() ); // Reserve a room for the asserting literal.

					// First deal with inverse of the last literal in trail (which was found in conflict.)
					// Then Start from the last literal in trail.
					while ( implicationPointCount > 0 )
					{
#ifdef ASSERT
						if ( clausePtr == NULL )
						{ printf("tId #%d bId #%d: (2) clausePtr == NULL, conflictLit #%d, currentTrailLit = #%d, index = %d, decisionLevelTrailIdPtr[%d] = %d, trailEndId = %d, implicationPointCount = %d\n", tId, bId, conflictLit.index(), currentTrailLit.index(), index, (decisionLevel-1), decisionLevelTrailIdPtr->at(decisionLevel-1), trailEndId, implicationPointCount ); }
#endif
						if ( clausePtr->get_learnt() == true )
						{
							atomicAdd( &__dev_clauseActivityKey[clausePtr->index()], __dev_claActivityIncreaseDelta );
							
							if ( __dev_clauseActivityKey[clausePtr->index()] > 1e20 )
							{ __dev_decreaseClauseActivity = 1; }
						}
						//__threadfence();

						for ( int i = 0; i < clausePtr->size(); ++i )
						{
							Lit q = clausePtr->data(i);

							if ( q.var() != currentTrailLit.var() )
							{
								if ( (get_varSeenMarker( tVarSeenMarker, q.var() ) == false) && (get_decisionLevel( tDecisionLevel, q.var() ) > 0) )
								{
									set_varSeenMarker( tVarSeenMarker, q.var(), true );
									if ( get_decisionLevel( tDecisionLevel, q.var() ) == decisionLevel )
									{ ++implicationPointCount; }
									else if ( get_decisionLevel( tDecisionLevel, q.var() ) > 0 )
									{
										learntClauseLitPtr->push_back( q );
										maxLearntLitLevel = max( maxLearntLitLevel, get_decisionLevel( tDecisionLevel, q.var() ) );
									}
								}
							}
							__threadfence_block();
						}
						// Select the next literal in the same decision level. Back from the last literal in trail.
						do
						{
							--index;
							currentTrailLit = get_trail( tTrail, index );
						}
						while( get_varSeenMarker( tVarSeenMarker, currentTrailLit.var() ) == false );

						clausePtr = get_antecedentPointer( tAntecedentPointer, currentTrailLit.var() );

						set_varSeenMarker( tVarSeenMarker, currentTrailLit.var(), false );
						--implicationPointCount;
						__threadfence_block();
					}

					learntClauseLitPtr->at(0) = currentTrailLit;
#ifdef ASSERT
					if ( (maxLearntLitLevel == 0) && (learntClauseLitPtr->size() != 1) )
					{ printf("tId #%d bId #%d: Assertion failed: Learnt clause size() = %d with maxLearntLitLevel = 0\n", tId, bId, learntClauseLitPtr->size() ); }
#endif
				} // if ( tId == 0 )
				__threadfence_block();

				// TODO: simplify the learnt clause like they do in MiniSAT.

				__shared__ Clause* learntClausePtr;
				
				if ( tId == 0 )
				{
					learntClausePtr = NULL;
					conflictLitCount += learntClauseLitPtr->size();

					if ( learntClauseLitPtr->size() > 1 )
					{
						int size = atomicMax( __dev_clausePtrIndexSize, 0 );

						if ( size >= __clausePtrIndexCapacity )
						{
							printf( "tId #%d bId #%d: __dev_clausePtrIndexSize = size = %d. Clause index is full.\n", tId, bId, size );
							doConflictAnalysis = false;
							doBCP = false;
							stopLoop = true;
							break;
						}
						else
						{
							size = atomicAdd( __dev_clausePtrIndexSize, 1 );
#ifdef DEBUG_CUDASAT
							printf("tId #%d bId #%d: size = %d, __dev_clausePtrIndexSize = %d.\n", tId, bId, size, (*__dev_clausePtrIndexSize) );
#endif
							learntClausePtr = Clause_new( size, true, learntClauseLitPtr->get_dataPtr(), 0, learntClauseLitPtr->size() );
							if ( learntClausePtr == NULL )
							{
								printf("Insufficient memory for any learnt clause.\n");
								doConflictAnalysis = false;
								doBCP = false;
								stopLoop = true;
								break;
							}

							// Find the second watch literal.
							Lit* secondWatchPtr = NULL;

							for ( int i = 0; i < learntClausePtr->size(); ++i )
							{
								if ( get_decisionLevel( tDecisionLevel, learntClausePtr->data(i).var() ) == maxLearntLitLevel )
								{
									secondWatchPtr = learntClausePtr->data_pointer(i);
									break;
								}
							}

							set_clausePtrIndex( size, learntClausePtr );
#ifdef DEBUG_CUDASAT
							printf("tId #%d bId #%d: __dev_clausePtrIndex[%d] = %x, clause index = %d.\n", tId, bId, size, get_clausePtrIndex(size), get_clausePtrIndex(size)->index() );
#endif
							// Update watch pointers and watch list.
							// The added leart clause won't take any effect until other solver check them into watch list.

							// The watch pointer #1 is one literal with maxLearntLitLevel.
							set_watchPointer( tWatchPointer, (size << 1), learntClausePtr->data_pointer(0) );
							set_watchPointer( tWatchPointer, ((size << 1) + 1), secondWatchPtr );

							get_watchList( tWatchList, (learntClausePtr->data_pointer(0))->index() )->push_back( learntClausePtr );
							get_watchList( tWatchList, secondWatchPtr->index() )->push_back( learntClausePtr );
							__threadfence();
#ifdef ASSERT
							if ( (learntClausePtr->data_pointer(0))->index() == secondWatchPtr->index() )
							{ printf("tId #%d bId #%d: Assertion failed: two watch pointers in a learnt clause is identical.\n", tId, bId ); }
#endif
						}
#ifdef DEBUG_CUDASAT
						printf("tId #%d bId #%d: add learnt clause: ", tId, bId );
						for ( int j = 0; j < learntClausePtr->size(); ++j )
						{
							printf( "Lit #%d %s, ", (learntClausePtr->data(j)).index(), ((j == 0) ? "(asserting)" : "") );
						}
						printf( "\n" );

						printf("tId #%d bId #%d: maxLearntLitLevel = %d, learntClauseCount = %d\n", tId, bId, maxLearntLitLevel, learntClauseCount );
#endif
					}
					else // learnt unit clause.
					{
						if ( learntClauseLitPtr->size() == 1 )
						{
#ifdef ASSERT
							if ( maxLearntLitLevel != 0 )
							{ printf("tId #%d bId #%d: Assertion failed: Learnt unit clause Lit #%d with maxLearntLitLevel = %d\n", tId, bId, learntClauseLitPtr->front().index(), maxLearntLitLevel ); }
#endif
							int litIndex = atomicCAS( &__dev_unitVar[learntClauseLitPtr->front().var()], -1, learntClauseLitPtr->front().index() );

							if ( litIndex == -1 )
							{
								int size = atomicMax( &__dev_unitClauseLitSize, 0 );

								if ( size < __dev_varNumber )
								{
									size = atomicAdd( &__dev_unitClauseLitSize, 1 );
									set_unitClauseLit( size, learntClauseLitPtr->front() );
									__threadfence();
#ifdef DEBUG_CUDASAT
									printf("tId #%d bId #%d: learnt unit clause Lit #%d. Add it into unitClauseLit[%d]\n", tId, bId, learntClauseLitPtr->front().index(), (learntClauseLitPtr->front()).var() );
#endif
								}
								else
								{ printf( "tId #%d bId #%d: __dev_unitClauseLitSize = %d. Unit clause index is full.\n", tId, bId, size ); }
							}
/*
							else
							{
								if ( learntClauseLitPtr->front().index() != litIndex )
								{
									set_satResult( bId, Lbool(false) );
#ifdef DEBUG_CRITICAL
									printf( "tId #%d bId #%d: (3) checked UNSAT.\n", tId, bId );
#endif
								}
							}
*/
							localUnitClausePtr->push_back( learntClauseLitPtr->front() );
						}
#ifdef ASSERT
						else
						{ printf("tId #%d bId #%d: Assertion failed. Learnt clause size = %d\n", tId, bId, learntClauseLitPtr->size() ); }
#endif
					}
				} // if ( tId == 0 )
				__threadfence_block();
				//__syncthreads();

				if ( stopLoop == true )
				{ break; }

				if ( (conflictCount >= conflictCountLimit)
					//|| (learntClauseCount >= learntClauseCountLimit)
					|| (get_satResult( bId ).convert_to_int() == __LBOOL_FALSE_INT) )
				{
					if ( tId == 0 )
					{
						doConflictAnalysis = false;
						doBCP = false;
						stopLoop = true;
					} // if ( tId == 0 )
					__threadfence_block();
					break;
				}

				// Undo corresponding variable assignment before back-tracking.
				for ( int i = tId + decisionLevelTrailIdPtr->at(maxLearntLitLevel); i < trailEndId; i += __threadsPerBlock )
				{
					Lit trailLit = get_trail( tTrail, i );
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: undo trail literal #%d: Lit #%d\n", tId, bId, i, trailLit.index() );
#endif
					set_varAssignment( tVarAssignment, trailLit.var(), Lbool() );
					//set_antecedentPointer( tAntecedentPointer, trailLit.var(), NULL );
					//set_decisionLevel( tDecisionLevel, trailLit.var(), -1 );
				}
				__syncthreads();

				// Setting variables for back-tracking.
				if ( tId == 0 )
				{
					order = decisionLevelVarOrderPtr->at(maxLearntLitLevel);
					trailEndId = decisionLevelTrailIdPtr->at(maxLearntLitLevel);
					decisionLevel = maxLearntLitLevel;
#ifdef DEBUG_CUDASAT
					printf( "tId #%d bId #%d: Back-tracking: trailEndId = %d: decisionLevel = %d\n", tId, bId, trailEndId, decisionLevel );
#endif
					propagationQueuePtr->clear();
					antecedentQueuePtr->clear();
					__threadfence_block();

					propagationQueuePtr->push_back( ~(learntClauseLitPtr->at(0)) );
					antecedentQueuePtr->push_back( learntClausePtr );
					__threadfence_block();

					tempQueuePtr->clear();
					tempAntecedentPtr->clear();
					tempWatchListPtr->clear();
					learntClauseLitPtr->clear();
				}
				__threadfence_block();
			} // if ( doConflictAnalysis == true )
			__threadfence_block();
		} // while ( doBCP == true )
		__threadfence_block();

		if ( stopLoop == true )
		{ break; }

		// Conflict analysis must assign a back-tracking order number before here.
		if ( get_satResult( bId ).convert_to_int() != __LBOOL_UNDEF_INT )
		{ break; } // BREAK: while ( order < __dev_varNumber )

		if ( tId == 0 )
		{
			if ( doConflictAnalysis == false )
			{
				++order;

				if ( trailEndId == __dev_varNumber )
				{
					set_satResult( bId, Lbool(true) );
#ifdef DEBUG_CRITICAL
					printf( "tId #%d bId #%d: (5) checked SAT.\n", tId, bId );
#endif
					break;
				}
			}
		} // if ( tId == 0 )
		__threadfence_block();
	} // while ( order < __dev_varNumber )
	__threadfence_block();

	if ( tId == 0 )
	{
#ifdef RANDOM_POLARITY
		__dev_randState[bId] = localCurandState;
#endif
		set_conflictCount( bId, conflictCount );
		set_decisionCount( bId, decisionCount );
		set_propagationCount( bId, propagationCount );
		set_conflictLitCount( bId, conflictLitCount );

		if ( (get_satResult( bId ).convert_to_int() == __LBOOL_TRUE_INT) || (order == __dev_varNumber) )
		{
			set_satResult( bId, Lbool(true) );
			atomicExch( &__dev_hasResult, 1 );
#ifdef DEBUG_CRITICAL
			printf( "tId #%d bId #%d: SAT, conflict / Limit = %d / %d, decision = %d, propagation = %d, conflictLit = %d, counter = %d\n", tId, bId, conflictCount, conflictCountLimit, decisionCount, propagationCount, conflictLitCount, counter );
#endif
		}
		else if ( get_satResult( bId ).convert_to_int() == __LBOOL_FALSE_INT )
		{
			atomicExch( &__dev_hasResult, 1 );
#ifdef DEBUG_CRITICAL
			printf( "tId #%d bId #%d: UNSAT, conflict / Limit = %d / %d, decision = %d, propagation = %d, conflictLit = %d, counter = %d\n", tId, bId, conflictCount, conflictCountLimit, decisionCount, propagationCount, conflictLitCount, counter );
#endif
		}
		else
		{
			set_satResult( bId, Lbool() );
#ifdef NO_IDLE_BLOCK
			atomicExch( &__dev_hasResult, 1 );
#endif
#ifdef HALF_IDLE_BLOCK
			atomicAdd( &__dev_idleBlockCount, 1 );
#endif
#ifdef DEBUG_CRITICAL
			printf( "tId #%d bId #%d: RESTART, conflict / Limit = %d / %d, decision = %d, propagation = %d, conflictLit = %d, counter = %d\n", tId, bId, conflictCount, conflictCountLimit, decisionCount, propagationCount, conflictLitCount, counter );
#endif
		}
	} // if ( tId == 0 )

	return;
}

#endif /* __SOLVER_KERNEL_H__ */
